ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:ecl(ds; da), m:.
(ecl-act(ds; da; m; x)([]))  False 

latex

Definitions

guard(T), sq_type(T), A, A  B, P  Q, P  Q, x:A. B(x), P  Q, x. t(x), t  T, P  Q, prop{i:l}, False, ecl-act(ds; da; m; x), P  Q, , x:A. B(x), ff, tt, if b then t else f fi , star-append(T; P; Q), x(s), subtype(S; T)

Lemmas

not functionality wrt iff, assert of bnot, eqff to assert, not wf, bnot wf, ecl-halt-nil, assert of eq int, eqtt to assert, assert wf, iff transitivity, bool sq, bool cases, concat wf, Id wf, Knd wf, fpf wf, eq int wf, ifthenelse wf, star-append wf, nat plus inc, iseg wf, nat plus wf, le wf, ecl-halt wf, append wf, append is nil, bool wf, ma-valtype wf, decl-state wf, ecl wf, false wf, event-info wf, ecl-act wf, iff wf, nat wf, ecl-induction